l:IdLnk, dt:fpf(Id; tg.Type), a:Id. sqequal(fpf-dom(Kind-deq; locl(a); lnk-decl(l; dt)); ff) 

latex

Definitions	x. t(x), Id, IdLnk, fpf(A; a.B(a)), lnk-decl(l; dt), fpf-dom(eq; x; f), sq_type(T), x:A. B(x), P  Q, guard(T), t  T, , deq-member(eq; x; L), ff, Kind-deq, map(f; as), P  Q, P  Q, locl(a), rcv(l,tg), Knd, (x  l), b, x:A. B(x), P  Q, False
Lemmas	not locl rcv, rcv wf, locl wf, Knd wf, member map, map wf, Kind-deq wf, assert-deq-member, bfalse wf, assert wf, deq-member wf, iff imp equal bool, bool sq, IdLnk wf, Id wf, fpf wf